Dynamic Consistency of Conditional Simple Temporal Networks via Mean Payoff Games: a Singly-Exponential Time DC-Checking

摘要

Conditional Simple Temporal Network (CSTN) is a constraint-basedgraph-formalism for conditional temporal planning. It offers a more flexibleformalism than the equivalent CSTP model of Tsamardinos, Vidal and Pollack,from which it was derived mainly as a sound formalization. Three notions ofconsistency arise for CSTNs and CSTPs: weak, strong, and dynamic. Dynamicconsistency is the most interesting notion, but it is also the most challengingand it was conjectured to be hard to assess. Tsamardinos, Vidal and Pollackgave a doubly-exponential time algorithm for deciding whether a CSTN isdynamically-consistent and to produce, in the positive case, a dynamicexecution strategy of exponential size. In the present work we offer a proofthat deciding whether a CSTN is dynamically-consistent is coNP-hard and providethe first singly-exponential time algorithm for this problem, also producing adynamic execution strategy whenever the input CSTN is dynamically-consistent.The algorithm is based on a novel connection with Mean Payoff Games, a familyof two-player combinatorial games on graphs well known for having applicationsin model-checking and formal verification. The presentation of such connectionis mediated by the Hyper Temporal Network model, a tractable generalization ofSimple Temporal Networks whose consistency checking is equivalent todetermining Mean Payoff Games. In order to analyze the algorithm we introduce arefined notion of dynamic-consistency, named \epsilon-dynamic-consistency, andpresent a sharp lower bounding analysis on the critical value of the reactiontime \hat{\varepsilon} where the CSTN transits from being, to not being,dynamically-consistent. The proof technique introduced in this analysis of\hat{\varepsilon} is applicable more in general when dealing with lineardifference constraints which include strict inequalities.